\begin{tabbing}
Q{-}R{-}glues(${\it es}$;${\it Ib\_valtype}$;$g$;$f$;${\it Ia}$;${\it Qa}$;${\it Ib}$;${\it Rb}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=weak{-}antecedent{-}surjection(${\it es}$;\{${\it Ib}$\};\{${\it Ia}$\};$g$) \& Q{-}R{-}pre{-}preserving(${\it es}$;$g$;\{${\it Ib}$\};${\it Qa}$;${\it Rb}$)\+
\\[0ex]\& Inj(\{$e$:es{-}E(${\it es}$)$\mid$ $\uparrow$($e$ $\in_{b}$ ${\it Ib}$)\} ;es{-}E(${\it es}$);$g$)
\\[0ex]\& ($\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Ib}$). $f$($g$($e$)) = ${\it Ib}$($e$) $\in$ ${\it Ib\_valtype}$)
\-
\end{tabbing}